$\forall$$k$:Knd, $x$:Id, $n$:top, $f$:(void$\rightarrow$void$\rightarrow$top).
\\[0ex]update{-}spec1($k$; $x$; $n$; $s$,$v$.$f$($s$,$v$)) $\in$ fpf((:Knd $\times$ Id); ${\it kz}$.top)